############################################################################
# This file mainly provides the `mathcomp` derivation, which is            #
# essentially a meta-package containing all core mathcomp libraries        #
# (ssreflect fingroup algebra solvable field character). They can be       #
# accessed individually through the passthrough attributes of mathcomp     #
# bearing the same names (mathcomp.ssreflect, etc).                        #
############################################################################
# Compiling a custom version of mathcomp using `mathcomp.override`.        #
# This is the replacement for the former `mathcomp_ config` function.      #
# See the documentation at doc/languages-frameworks/coq.section.md.        #
############################################################################

{
  lib,
  ncurses,
  graphviz,
  lua,
  fetchzip,
  mkCoqDerivation,
  withDoc ? false,
  single ? false,
  coq,
  hierarchy-builder,
  stdlib,
  version ? null,
}@args:

let
  repo = "math-comp";
  owner = "math-comp";
  withDoc = single && (args.withDoc or false);
  defaultVersion =
    let
      case = case: out: { inherit case out; };
      inherit (lib.versions) range;
    in
    lib.switch coq.coq-version [
      (case (range "8.20" "9.1") "2.5.0")
      (case (range "8.20" "9.1") "2.4.0")
      (case (range "8.19" "9.0") "2.3.0")
      (case (range "8.17" "8.20") "2.2.0")
      (case (range "8.17" "8.18") "2.1.0")
      (case (range "8.17" "8.18") "2.0.0")
      (case (range "8.19" "8.20") "1.19.0")
      (case (range "8.17" "8.18") "1.18.0")
      (case (range "8.15" "8.18") "1.17.0")
      (case (range "8.13" "8.18") "1.16.0")
      (case (range "8.14" "8.16") "1.15.0")
      (case (range "8.11" "8.15") "1.14.0")
      (case (range "8.11" "8.15") "1.13.0")
      (case (range "8.10" "8.13") "1.12.0")
      (case (range "8.7" "8.12") "1.11.0")
      (case (range "8.7" "8.11") "1.10.0")
      (case (range "8.7" "8.11") "1.9.0")
      (case (range "8.7" "8.9") "1.8.0")
      (case (range "8.6" "8.9") "1.7.0")
      (case (range "8.5" "8.7") "1.6.4")
    ] null;
  release = {
    "2.5.0".sha256 = "sha256-M/6IP4WhTQ4j2Bc8nXBXjSjWO08QzNIYI+a2owfOh+8=";
    "2.4.0".sha256 = "sha256-A1XgLLwZRvKS8QyceCkSQa7ue6TYyf5fMft5gSx9NOs=";
    "2.3.0".sha256 = "sha256-wa6OBig8rhAT4iwupSylyCAMhO69rADa0MQIX5zzL+Q=";
    "2.2.0".sha256 = "sha256-SPyWSI5kIP5w7VpgnQ4vnK56yEuWnJylNQOT7M77yoQ=";
    "2.1.0".sha256 = "sha256-XDLx0BIkVRkSJ4sGCIE51j3rtkSGemNTs/cdVmTvxqo=";
    "2.0.0".sha256 = "sha256-dpOmrHYUXBBS9kmmz7puzufxlbNpIZofpcTvJFLG5DI=";
    "1.19.0".sha256 = "sha256-3kxS3qA+7WwQkXoFC/+kq3OEkv4kMEzQ/G3aXPsp1Q4=";
    "1.18.0".sha256 = "sha256-mJJ/zvM2WtmBZU3U4oid/zCMvDXei/93v5hwyyqwiiY=";
    "1.17.0".sha256 = "sha256-bUfoSTMiW/GzC1jKFay6DRqGzKPuLOSUsO6/wPSFwNg=";
    "1.16.0".sha256 = "sha256-gXTKhRgSGeRBUnwdDezMsMKbOvxdffT+kViZ9e1gEz0=";
    "1.15.0".sha256 = "1bp0jxl35ms54s0mdqky15w9af03f3i0n06qk12k4gw1xzvwqv21";
    "1.14.0".sha256 = "07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9";
    "1.13.0".sha256 = "0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri";
    "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp";
    "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c";
    "1.10.0".sha256 = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
    "1.9.0".sha256 = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r";
    "1.8.0".sha256 = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
    "1.7.0".sha256 = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
    "1.6.4".sha256 = "09ww48qbjsvpjmy1g9yhm0rrkq800ffq21p6fjkbwd34qvd82raz";
    "1.6.1".sha256 = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
  };
  releaseRev = v: "mathcomp-${v}";

  # list of core mathcomp packages sorted by dependency order
  packages = {
    "boot" = [ ];
    "order" = [ "boot" ];
    "fingroup" = [ "boot" ];
    "ssreflect" = [
      "boot"
      "order"
    ];
    "algebra" = [
      "order"
      "fingroup"
    ];
    "solvable" = [ "algebra" ];
    "field" = [ "solvable" ];
    "character" = [ "field" ];
    "all" = [ "character" ];
  };

  mathcomp_ =
    package:
    let
      mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
      pkgpath = if package == "single" then "." else package;
      pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
      pkgallMake = ''
        echo "all.v"  > Make
        echo "-I ." >>   Make
        echo "-R . mathcomp.all" >> Make
      '';
      derivation = mkCoqDerivation (
        {
          inherit
            version
            pname
            defaultVersion
            release
            releaseRev
            repo
            owner
            ;

          mlPlugin = lib.versions.isLe "8.6" coq.coq-version;
          nativeBuildInputs = lib.optionals withDoc [
            graphviz
            lua
          ];
          buildInputs = [ ncurses ];
          propagatedBuildInputs = mathcomp-deps;

          buildFlags = lib.optional withDoc "doc";

          preBuild = ''
            if [[ -f etc/utils/ssrcoqdep ]]
            then patchShebangs etc/utils/ssrcoqdep
            fi
            if [[ -f etc/buildlibgraph ]]
            then patchShebangs etc/buildlibgraph
            fi
          ''
          + ''
            # handle mathcomp < 2.4.0 which had an extra base mathcomp directory
            test -d mathcomp && cd mathcomp
            cd ${pkgpath} || cd ssreflect  # before 2.5, boot didn't exist, make it behave as ssreflect
          ''
          + lib.optionalString (package == "all") pkgallMake;

          meta = {
            homepage = "https://math-comp.github.io/";
            license = lib.licenses.cecill-b;
            maintainers = with lib.maintainers; [
              vbgl
              jwiegley
              cohencyril
            ];
          };
        }
        // lib.optionalAttrs (package != "single") { passthru = lib.mapAttrs (p: _: mathcomp_ p) packages; }
        // lib.optionalAttrs withDoc {
          htmldoc_template = fetchzip {
            url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip";
            sha256 = "0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8";
          };
          postBuild = ''
            cp -rf _build_doc/* .
            rm -r _build_doc
          '';
          postInstall =
            let
              tgt = "$out/share/coq/${coq.coq-version}/";
            in
            lib.optionalString withDoc ''
              mkdir -p ${tgt}
              cp -r htmldoc ${tgt}
              cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/
            '';
          buildTargets = "doc";
          extraInstallFlags = [ "-f Makefile.coq" ];
        }
      );
      patched-derivation1 = derivation.overrideAttrs (
        o:
        lib.optionalAttrs
          (
            o.pname != null
            && o.pname == "mathcomp-all"
            && o.version != null
            && o.version != "dev"
            && lib.versions.isLt "1.7" o.version
          )
          {
            preBuild = "";
            buildPhase = "";
            installPhase = "echo doing nothing";
          }
      );
      patched-derivation2 = patched-derivation1.overrideAttrs (
        o:
        lib.optionalAttrs
          (
            lib.versions.isLe "8.7" coq.coq-version || (o.version != "dev" && lib.versions.isLe "1.7" o.version)
          )
          {
            installFlags = o.installFlags ++ [ "-f Makefile.coq" ];
          }
      );
      patched-derivation3 = patched-derivation2.overrideAttrs (
        o:
        lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.0.0" o.version))
          {
            propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
          }
      );
      patched-derivation4 = patched-derivation3.overrideAttrs (
        o:
        lib.optionalAttrs (o.version != null && o.version == "2.3.0") {
          propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
        }
      );
      # boot and order packages didn't exist before 2.5,
      # so make boot behave as ssreflect then (c.f., above)
      # and building nothing in order and ssreflect
      patched-derivation5 = patched-derivation4.overrideAttrs (
        o:
        lib.optionalAttrs
          (
            lib.elem package [
              "order"
              "ssreflect"
            ]
            && o.version != null
            && o.version != "dev"
            && lib.versions.isLt "2.5" o.version
          )
          {
            preBuild = "";
            buildPhase = "echo doing nothing";
            installPhase = "echo doing nothing";
          }
      );
    in
    patched-derivation5;
in
mathcomp_ (if single then "single" else "all")
